/* Map a physical frame in for a given PTE */

#include "include.h"

static int _new_seL4_pt(sos_pcb *pcb, seL4_Word proc_vaddr);
static seL4_CapRights _page_attrs_caprights(page_attrs attrs);
static seL4_ARM_VMAttributes _page_attrs_vmattrs(page_attrs attrs);
static int _pte_is_alloced(page_table_entry pte);
static int _pte_is_mapped(page_table_entry pte);
static int _attrs_are_empty(page_attrs attrs);

/* Perform seL4-level mapping of a frame (at proc_cap) to pcb's proc_vaddr */
int sos_page_map(sos_pcb *pcb, seL4_Word proc_vaddr, seL4_Word proc_cap) {
    int err;
    sos_region *region;
    seL4_CapRights rights;
    seL4_ARM_VMAttributes vmattrs;

    assert(pcb != 0 && proc_cap != 0 && pcb->seL4_pd != 0);

    // Get attributes
    err = sos_resolve_region(&(pcb->regions), proc_vaddr, &region);
    if (err != SOS_REGION_SUCCESS) return SOS_PAGE_TABLE_SEGFAULT;

    // Translate SOS attributes into seL4 CapRights
    rights = _page_attrs_caprights(region->attrs);
    vmattrs = _page_attrs_vmattrs(region->attrs);

    // Map frame into process seL4 vspace
    dprintf(5, "Mapping frame at %p\n", (void*) PAGE_ALIGN(proc_vaddr));
    err = seL4_ARM_Page_Map(proc_cap, pcb->seL4_pd,
                            PAGE_ALIGN(proc_vaddr), rights, vmattrs);
    dprintf(7, "Done mapping frame\n");
    if (err == seL4_FailedLookup) {
        dprintf(7, "Need new PT\n");
        // We need to allocate a new seL4 page table object
        err = _new_seL4_pt(pcb, proc_vaddr);
        if (err) {
            // Failed to get a free frame for the seL4 page table.
            // We should really have a scratch reserve for this situation.
            dprintf(6, "page_map: Could not get frame for seL4 PT\n");
            return SOS_PAGE_TABLE_SEGFAULT;
        }

        // Retry the original mapping
        dprintf(7, "page_map: retrying with fresh PT\n");
        err = seL4_ARM_Page_Map(proc_cap, pcb->seL4_pd,
                                PAGE_ALIGN(proc_vaddr), rights, vmattrs);
        if (err) {
            // XXX Free the frame
            return SOS_PAGE_TABLE_SEGFAULT;
        }
    }
    dprintf(7, "sos_page_map: returning\n");
    return SOS_PAGE_TABLE_SUCCESS;
}

/* Pull the frame at proc_cap from the process address space. */
/* We don't update the page table - if the address faults, we restore by */
/* calling frame_reference */
int sos_page_unmap(sos_pcb *pcb, seL4_Word proc_vaddr, seL4_Word proc_cap) {
    // XXX do we need to delete cap from cspace?
    return seL4_ARM_Page_Unmap(proc_cap);
}



/* Allocate and map in a new seL4 page table object */
/* This is fully synchronous - i.e. if we're out of memory, process goes boom. */
/* XXX Update to use scratch pool. */
static int _new_seL4_pt(sos_pcb *pcb, seL4_Word proc_vaddr) {
    int err;
    // On ARM, PageTableBits = 10, so frame_alloc is not appropriate.
    dprintf(7, "attempting ut_alloc...\n");
    seL4_Word pt_addr = ut_alloc(seL4_PageTableBits);
    seL4_CPtr pt_cap;
    if (pt_addr == 0) {
        dprintf(7, "ut is oom\n");
        return FRAME_TABLE_OOM;
    }

    // Retype it into a seL4 page table
    dprintf(7, "retyping to seL4_PageTableObject\n");
    err = cspace_ut_retype_addr(pt_addr, seL4_ARM_PageTableObject,
                                seL4_PageTableBits, cur_cspace, &pt_cap);
    if (err) {
        // Something's gone wrong - we've made a bad assumption somewhere
        dprintf(1, "fault handler: Failed to retype seL4 PTO\n");
        return SOS_PAGE_TABLE_ERROR;
    }

    // Attach it to the process address space
    dprintf(7, "Mapping pagetable\n");
    err = seL4_ARM_PageTable_Map(pt_cap, pcb->seL4_pd, PAGE_ALIGN(proc_vaddr),
                                 seL4_ARM_Default_VMAttributes);
    if (err) {
        // We badly misunderstand something about seL4
        dprintf(1, "fault handler: Failed to map in seL4 PTO\n");
        return SOS_PAGE_TABLE_ERROR;
    }

    // Store the seL4 page table cap into the pt_caps list, so it can be freed
    dprintf(7, "Storing PT cap\n");
    err = sos_pt_list_insert(pt_addr, pt_cap, &(pcb->pt_caps));
    if (err) {
        // ut is out of memory
        // XXX We should probably clean up some resources here
        dprintf(1, "fault handler: Failed to store new cap in list\n");
        return SOS_PAGE_TABLE_ERROR;
    }


    dprintf(6, "new_sel4_pt: got PT frame\n");

    return SOS_PAGE_TABLE_SUCCESS;
}

static seL4_CapRights _page_attrs_caprights(page_attrs attrs) {
    seL4_CapRights ret = 0;
    if (attrs.writeable) ret |= seL4_CanWrite;
    if (attrs.readable)  ret |= seL4_CanRead;
    return ret;
}

static seL4_ARM_VMAttributes _page_attrs_vmattrs(page_attrs attrs) {
    seL4_ARM_VMAttributes ret = seL4_ARM_Default_VMAttributes;
    if (attrs.executable == 0) ret |= seL4_ARM_ExecuteNever;
    return ret;
}

static inline int _pte_is_alloced(page_table_entry pte) {
    // If any attr bits are set
    return (!_attrs_are_empty(pte.attrs));
}

static inline int _pte_is_mapped(page_table_entry pte) {
    // If bits set and frame number nonzero
    // XXX This is wrong
    return (!_attrs_are_empty(pte.attrs) && pte.framenumber != 0);
}
